i:, j:{...i}. j  i 

latex

ProofTree

Definitions	True, T, t  T, x:A. B(x), P  Q, SqStable(P), {...i}
Lemmas	int lower wf, decidable le, le wf, sq stable from decidable